\begin{tabbing}
ecl{-}es{-}act(${\it es}$; $m$; $x$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$ecl\_ind(\=$x$;\+
\\[0ex]$k$,${\it test}$.($\lambda$$e_{1}$,$e_{2}$. False);
\\[0ex]$a$,$b$,${\it aa}$,${\it ab}$.($\lambda$$e_{1}$,$e_{2}$. (${\it aa}$($e_{1}$,$e_{2}$))
\\[0ex]$\vee$ $\exists$$e$$\in$($e_{1}$,$e_{2}$].(ecl{-}es{-}halt(${\it es}$; $a$)(0,$e_{1}$,es{-}pred(${\it es}$; $e$))) $\wedge$ (${\it ab}$($e$,$e_{2}$)));
\\[0ex]$a$,$b$,${\it aa}$,${\it ab}$.($\lambda$$e_{1}$,$e_{2}$. ((${\it aa}$($e_{1}$,$e_{2}$))
\\[0ex]$\wedge$ l{-}all(ecl{-}ex($b$); $n$.$\forall$$e$$\in$[$e_{1}$,$e_{2}$).$\neg$(ecl{-}es{-}halt(${\it es}$; $b$)($n$,$e_{1}$,$e$))))
\\[0ex]$\vee$ \=((${\it ab}$($e_{1}$,$e_{2}$))\+
\\[0ex]$\wedge$ l{-}all(ecl{-}ex($a$); $n$.$\forall$$e$$\in$[$e_{1}$,$e_{2}$).$\neg$(ecl{-}es{-}halt(${\it es}$; $a$)($n$,$e_{1}$,$e$)))));
\-\\[0ex]$a$,$b$,${\it aa}$,${\it ab}$.($\lambda$$e_{1}$,$e_{2}$. ((${\it aa}$($e_{1}$,$e_{2}$))
\\[0ex]$\wedge$ l{-}all(cons(0; ecl{-}ex($b$)); $n$.$\forall$$e$$\in$[$e_{1}$,$e_{2}$).$\neg$(ecl{-}es{-}halt(${\it es}$; $b$)($n$,$e_{1}$,$e$))))
\\[0ex]$\vee$ \=((${\it ab}$($e_{1}$,$e_{2}$))\+
\\[0ex]$\wedge$ l{-}all(cons(0; ecl{-}ex($a$)); $n$.$\forall$$e$$\in$[$e_{1}$,$e_{2}$).$\neg$(ecl{-}es{-}halt(${\it es}$; $a$)($n$,$e_{1}$,$e$)))));
\-\\[0ex]$a$,${\it aa}$.($\lambda$$e_{1}$,$e_{2}$. [$e_{1}$;$e_{2}$]$\sim$([$x$,$y$].ecl{-}es{-}halt(${\it es}$; $a$)(0,$x$,$y$))$\ast$[$x$,$y$].${\it aa}$($x$,$y$));
\\[0ex]$a$,$n$,${\it aa}$.if ($m$ =$_{0}$ $n$) then ecl{-}es{-}halt(${\it es}$; $a$)(0) else ${\it aa}$ fi ;
\\[0ex]$a$,$n$,${\it aa}$.${\it aa}$;
\\[0ex]$a$,$l$,${\it aa}$.${\it aa}$)
\-
\end{tabbing}